fix(docker): add openshell-prover to Dockerfile skeleton stages and provide z3#800
Merged
fix(docker): add openshell-prover to Dockerfile skeleton stages and provide z3#800
Conversation
|
🌿 Preview your docs: https://nvidia-preview-pr-800.docs.buildwithfern.com/openshell |
pimlock
previously approved these changes
Apr 10, 2026
The openshell-prover crate was added as a dependency of openshell-cli in #741 but the Docker build infrastructure was not updated. Cargo workspace resolution requires every crate manifest to be present even when only building a subset of packages. Add openshell-prover Cargo.toml, mkdir, and stub lib.rs to the skeleton stages of all affected Dockerfiles. Also add the previously missing openshell-policy and openshell-tui entries to the python-wheels Dockerfiles where they were absent.
The openshell-prover crate depends on z3. For Linux-targeted builds (python-wheels), install libz3-dev to link against the system library. For macOS cross-compilation (python-wheels-macos, cli-macos), compile z3 from source via the bundled-z3 feature since system libz3-dev only provides a Linux .so, not a macOS .dylib. Add a bundled-z3 forwarding feature to openshell-cli so both cargo and maturin can activate it uniformly.
…ndgen Switch all CLI builds to bundled-z3 (compile z3 from source) instead of relying on system libz3-dev. This is required because: - Linux musl CLI builds cannot link against glibc libz3.so - macOS cross-compilation has no system z3 available - Distributable Python wheels should not depend on runtime libz3 Add libclang-dev to all CLI Dockerfiles since z3-sys uses bindgen which requires libclang at compile time. Add openshell-prover to the sed workspace scope in both release workflows so Cargo can resolve the path dependency from openshell-cli.
…compiler musl-tools only provides musl-gcc (C compiler wrapper), not musl-g++. The z3 bundled cmake build needs a C++ compiler to compile z3 from source. Use the system g++ since z3 exposes a C-linkage API and libstdc++ is statically linked in the final musl binary.
Using system g++ directly produces object files with glibc symbols like __printf_chk that don't exist in musl. Instead, create a musl-g++ wrapper that mirrors musl-gcc: it invokes g++ with the musl-gcc.specs file, which redirects include and library paths to musl. This ensures z3 compiles against musl headers and avoids glibc symbol references.
The musl-gcc.specs approach strips all system include paths via -nostdinc, which removes C++ standard library headers and breaks std::atomic detection in z3's cmake build. Simpler approach: the only glibc-specific symbols z3 was pulling in were __printf_chk and similar __*_chk functions generated by _FORTIFY_SOURCE hardening. Disabling _FORTIFY_SOURCE makes g++ emit standard printf/memcpy/etc. calls that musl provides, while keeping all C++ headers intact.
In Alpine, Rust build scripts are compiled for the musl host target which defaults to static linking. Static musl binaries cannot dlopen, causing bindgen to fail when loading libclang.so for z3 FFI generation. Set CARGO_HOST_RUSTFLAGS="-C target-feature=-crt-static" so build scripts are dynamically linked (can dlopen) while the target CLI binary stays static.
Replace the Alpine Docker-in-Docker approach (Dockerfile.cli-musl) with direct-on-host builds using zig cc/c++ to target musl. This eliminates: - Docker-in-Docker overhead and cache mount complexity - The libclang dlopen failure in Alpine (static musl binaries cannot dlopen) - ~15 min z3 C++ compilation without sccache Zig provides a first-class musl-targeting C/C++ toolchain that avoids glibc contamination (no _FORTIFY_SOURCE symbols) while running natively on the glibc CI host where bindgen/libclang and sccache work normally.
cc-rs automatically injects --target=<rust-triple> (e.g. aarch64-unknown-linux-musl) when invoking clang-like compilers. Zig cannot parse the 'unknown' vendor component in Rust target triples. The wrapper scripts now filter out any --target flags from the arguments and rely solely on the zig-native target specified by the wrapper itself.
Zig's linker provides its own musl CRT startup objects (_start, _start_c) which conflict with Rust's self-contained musl CRT objects. Only use zig for compiling C/C++ source (z3, ring); the system gcc works correctly as the linker since Rust supplies its own musl sysroot.
Zig's C++ compiler uses libc++ while the system linker expects libstdc++, causing unresolved std::__1::* symbols from z3. Replace zig with a simple g++ wrapper that disables _FORTIFY_SOURCE — the only glibc-specific flag that produces symbols absent from musl (__printf_chk, __memcpy_chk, etc.). System gcc handles linking correctly since Rust provides its own musl CRT objects and libc.
cc-rs probes for aarch64-linux-musl-gcc by default, which does not exist on the Ubuntu CI host. Set CC_<target> explicitly to a wrapper that also disables _FORTIFY_SOURCE for consistency with the CXX wrapper.
Configure Linux musl release jobs to compile and link with zig wrappers, normalize cc-rs target flags, disable Rust self-contained musl linking, and link z3 against libc++ via CXXSTDLIB=c++. This avoids glibc symbol leaks from host g++ while keeping the build off Docker.
Python wheel cross-builds now compile bundled z3, which invokes CMake with CXX_<target>. The cross toolchain setup installed only gcc, so aarch64-linux- gnu-g++/x86_64-linux-gnu-g++ were missing and z3-sys failed at configure time. Install matching g++ cross compilers alongside gcc.
The osxcross SDK headers gate std::to_chars behind macOS 13.3+. Bundled z3 builds in macOS-targeted Docker images were compiling with -mmacosx-version-min=11.0, causing C++ availability errors in libc++. Set MACOSX_DEPLOYMENT_TARGET and target C/C++ flags to 13.3.
591b6cc to
d33f850
Compare
drew
approved these changes
Apr 10, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
The openshell-prover crate was added in #741 as a dependency of openshell-cli but the Docker build infrastructure was not updated, breaking all Docker builds that resolve the workspace.
Related Issue
Regression from #741.
Changes
openshell-proverCargo.toml,mkdir, and stublib.rsto the skeleton stages of all affected Dockerfiles (Dockerfile.images,Dockerfile.python-wheels,Dockerfile.python-wheels-macos,Dockerfile.cli-macos)openshell-policyandopenshell-tuiskeleton entries in the python-wheels Dockerfiles (also path deps of openshell-cli)libz3-devtoDockerfile.python-wheelsfor native Linux z3 linkingcmaketoDockerfile.python-wheels-macosand enable--features bundled-z3on both macOS cross-compile Dockerfiles to compile z3 from source (systemlibz3-devonly provides a Linux.so, not a macOS.dylib)bundled-z3forwarding feature toopenshell-cliso bothcargo buildandmaturin buildcan activate it uniformlyTesting
mise run pre-commitpassesChecklist